Finitary coalgebraic logics [PhD Thesis]

1 Introduction 1
1.1 Coalgebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1.1 Finite vs. infinite words . . . . . . . . . . . . . . . . . . . . 1
1.1.2 Formal definition . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Specifying coalgebras using modal logic . . . . . . . . . . . . . . . . 5
1.2.1 Why using modal languages? . . . . . . . . . . . . . . . . . 5
1.2.2 Coalgebraic modal logics . . . . . . . . . . . . . . . . . . . . 5
1.2.3 Issues concerning finitary modal languages . . . . . . . . . . 7
1.3 Our contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.3.1 Stone coalgebras . . . . . . . . . . . . . . . . . . . . . . . . 8
1.3.2 Algebraic semantics of coalgebraic modal logic . . . . . . . . 9
1.3.3 Coalgebraic logics and coalgebra automata . . . . . . . . . . 9
1.4 Origin of the presented material . . . . . . . . . . . . . . . . . . . . 9
2 Coalgebraic Modal Logics 11
2.1 Inductively defined logics . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1.1 Kripke polynomial functors . . . . . . . . . . . . . . . . . . 11
2.1.2 The logic MSML . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Logics given by predicate liftings . . . . . . . . . . . . . . . . . . . . 17
2.2.1 Syntax and semantics . . . . . . . . . . . . . . . . . . . . . . 18
2.2.2 Derivability and the logic L(Λ, Ax) . . . . . . . . . . . . . . . 22
2.2.3 The language of all liftings . . . . . . . . . . . . . . . . . . . 24
2.3 Coalgebraic fixed-point logic . . . . . . . . . . . . . . . . . . . . . . 26
2.3.1 Finitary coalgebraic logic . . . . . . . . . . . . . . . . . . . 26
2.3.2 Adding fixed-points . . . . . . . . . . . . . . . . . . . . . . 29
2.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3 Stone coalgebras 33
3.1 Stone duality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.1.1 Basic Stone duality . . . . . . . . . . . . . . . . . . . . . . . 35
3.1.2 Duality for modal algebras . . . . . . . . . . . . . . . . . . . 37
3.1.3 Modal logic is expressive for descriptive general frames . . . 41
3.2 From Kripke to Vietoris . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.3 Vietoris polynomial functors . . . . . . . . . . . . . . . . . . . . . . 48
3.3.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.3.2 Linking algebraic and coalgebraic semantics . . . . . . . . . 53
3.4 Duality between BAOT and Coalg(V) . . . . . . . . . . . . . . . . . 56
3.5 Alternative view: Many-sorted algebras . . . . . . . . . . . . . . . . 63
3.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4 Algebraic semantics of coalgebraic modal logic 71
4.1 Definition of the algebraic semantics . . . . . . . . . . . . . . . . . . 73
4.1.1 Algebras for an algebraic theory . . . . . . . . . . . . . . . . 73
4.1.2 (Pre-)Boolean algebras . . . . . . . . . . . . . . . . . . . . . 75
4.1.3 Liftings and the functor L . . . . . . . . . . . . . . . . . . . 80
4.1.4 Equivalence of Alg(T(Λ, Ax)) and Alg(L) . . . . . . . . . . . 84
4.2 Functor sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
4.2.1 The initial sequence of L . . . . . . . . . . . . . . . . . . . . 88
4.2.2 The final sequence of T . . . . . . . . . . . . . . . . . . . . 93
4.3 Coalgebraic semantics as a natural transformation . . . . . . . . . . . 95
4.3.1 Definition of δ . . . . . . . . . . . . . . . . . . . . . . . . . 96
4.3.2 A functor linking algebraic and coalgebraic semantics . . . . 97
4.3.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . 99
4.4 A characterization of duality . . . . . . . . . . . . . . . . . . . . . . 104
4.4.1 Existence of δ and injectivity . . . . . . . . . . . . . . . . . . 105
4.4.2 Surjectivity . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
4.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
5 Closure properties of coalgebra automata 113
5.1 Coalgebra automata . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
5.1.1 Deterministic graph automata . . . . . . . . . . . . . . . . . 114
5.1.2 The bisimulation game . . . . . . . . . . . . . . . . . . . . . 116
5.1.3 Coalgebra automata . . . . . . . . . . . . . . . . . . . . . . 117
5.2 Closure properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
5.2.1 Closure under union, intersection and projection . . . . . . . 121
5.2.2 From alternating automata to nondeterministic ones . . . . . . 125
5.2.3 Non-emptiness of coalgebra automata . . . . . . . . . . . . . 136
5.2.4 A remark about standardness . . . . . . . . . . . . . . . . . . 138
5.3 The connection with coalgebraic fixed-point logic . . . . . . . . . . . 140
5.3.1 Finite model property . . . . . . . . . . . . . . . . . . . . . . 141
5.3.2 A distributive law . . . . . . . . . . . . . . . . . . . . . . . . 142
5.4 Concluding remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . 145
A Category theory 147
A.1 Basic notions of category theory . . . . . . . . . . . . . . . . . . . . 147
A.2 Set-functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
A.2.1 Basic constructions . . . . . . . . . . . . . . . . . . . . . . . 148
A.2.2 Standard and weak pullback preserving functors . . . . . . . 149
A.3 Coalgebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
B Universal Algebra 157
B.1 Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
B.2 Equational Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159
C Parity games 163
Bibliography 171
Index 179